%% Technical Report for the work on the AI-DSL over the period of May
%% to September 2022.

\documentclass[]{report}
\usepackage{amssymb}
\usepackage{url}
\usepackage{minted}
\usepackage[textsize=footnotesize]{todonotes}
\newcommand{\nil}[2][]{\todo[color=purple,author=nil, #1]{#2}}
\usepackage[hyperindex,breaklinks]{hyperref}
\usepackage{breakurl}
\usepackage{listings}
\lstset{basicstyle=\ttfamily\footnotesize,breaklines=false,frame=single}
\usepackage{float}
\restylefloat{table}
\usepackage{longtable}
\usepackage{graphicx}
\usepackage[font=small,labelfont=bf]{caption}
\usepackage[skip=0pt]{subcaption}
\usepackage{circledsteps}

\begin{document}

\title{AI-DSL Technical Report\\(May to September 2022)
  % \[\texttt{DRAFT}\]
}
\author{Nil Geisweiller, Matthew Ikl\'e, Deborah Duong, Samuel Roberti}
\maketitle

\begin{abstract}
  This report describes the second phase of the research that has
  taken place towards developing an AI-DSL for the SingularityNET
  platform.  It focuses primarily on experimenting with the
  formalization of mathematical properties of AI algorithms, in
  particular a descending property for the gradient descent algorithm,
  using the Dependently Typed Language (DTL) Idris.  It then turns to
  program synthesis applied to the problem of automatically composing
  AI services to meet a particular specification.  In conclusion, it
  contains a description of related work as well as directions for
  future work.
\end{abstract}

\tableofcontents

\chapter{Introduction}

\section{Setting the Scene}

In the previous iteration we explored using Dependent Types to express
formal specifications of AI services, with the ultimate goal of
building a language for easily writing those specifications, the
AI-DSL itself, as well as services to automatically connect AI
services together, the AI-DSL Registry~\cite{AIDSLReport2021}.

Back then we experimented with trivial AI services, computing simple
arithmetic, described by trivial properties, such as the parity of
their inputs/outputs.  We were able to demonstrate that Idris, our DTL
of choice, can be used to verify the correctness of such AI service
assemblages.  The approach seemed promising, but to really put the
idea to the test we had to make progress on two fronts:

\begin{enumerate}
\item Replace trivial AI services by actual AI algorithms.
\item Explore program synthesis, as it became clear that it is at the
  heart of this endeavor.  First, for building the AI service
  assemblages themselves.  Second, for achieving fuzzy matching, that
  is when an AI service almost fits a specification but not quite, or
  when AI services almost get together but not quite.  And third, for
  potentially synthesizing AI services from the ground up.
\end{enumerate}
That is what we have done during that iteration.

\section{Work Accomplished}

First we have implemented three AI algorithms in Idris:
\begin{enumerate}
\item Gradient descent
\item Linear regression
\item Logistic regression
\end{enumerate}
These algorithms were chosen because they are relatively simple, yet
extensively use in real world applications, as well as tightly related
to each other.  Linear regression can be framed as a gradient descent
problem, and logistic regression can be framed both as gradient
descent and linear regression problems, thus constituting an excellent
case study for the AI-DSL.  Alongside these implementations, a
descending property was formulated and formally proved for each
algorithm.

Finally, we have explored ways to perform program synthesis of
dependently typed programs.  While we have only achieved partial
success as far as program synthesis is concerned, we were able to
demonstrate its feasibility within the Idris ecosystem.  It was clear
from the start anyway that to be done well and fully, program
synthesis essentially requires achieving AGI.  Indeed, it is one of
these AI-complete problems.  That is, any problem can be framed as a
program synthesis problem and vice versa.  The idea being that such
functionality can be progressively grown, deferred less and less to
human intervention, as the network of AI services and the AI-DSL
evolve.

The report also contains an extensive, though somewhat packed, section
of related work in the concluding chapter as well directions for the
future phases.

\chapter{Implementation and Verification of AI Algorithms}

\section{Implementation of AI Algorithms}
We have implemented the following AI algorithms in Idris:
\begin{enumerate}
\item Descent: a generic descending algorithm.
\item Gradient Descent: a gradient descent algorithm using Descent.
\item Linear Regression: a linear regression algorithm using Gradient
  Descent.
\item Logistic Regression: a logistic regression algorithm using
  Gradient Descent.
\item Logistic-Linear Regression: a logistic regression algorithm
  using Linear Regression.
\end{enumerate}
\begin{figure}[H]
  \centering
  \includegraphics[scale=0.8]{figs/ai-algorithms.xfig.pdf}
  \caption{AI algorithms call graph}
  \label{fig:ai_algorithms}
\end{figure}
A call graph is provided in Figure~\ref{fig:ai_algorithms}.  Each
algorithm may be viewed as an AI service, together forming a network
of AI services delegating work to one another when possible.

The idea of performing logistic regression via two paths, either
directly via calling Gradient Descent, or indirectly via calling
Linear Regression, came from the ambition of having our AI-DSL
prototype discover an alternate way, possibly unforeseen by the AI
practitioner, to perform certain AI tasks, here logistic regression.
As we will see we did not come far enough to achieve that, but we
certainly keep that goal on the side for the future.

Let us now describe in more details what each algorithm is doing, and
then provide the descending property we have focused on during this
work.

\subsection{Descent}
The Descent algorithm takes the following inputs:
\begin{enumerate}
\item a cost function to minimize;
\item a step function to jump from candidate to candidate, also called
  update function;
\item an initial candidate to start the search from;
\item a maximum number of steps allocated to the search.
\end{enumerate}
It outputs the final candidate as well as the remaining unallocated
steps.  Essentially the Descent algorithm descends as long as the next
candidate is better than the previous one or the maximum number of
steps allocated to the search as been reached.

\subsection{Gradient Descent}
The Gradient Descent algorithm takes the following inputs:
\begin{enumerate}
\item a loss function;
\item a gradient function;
\item a learning rate, also called step size;
\item an initial candidate to start the search from;
\item a maximum number of steps allocated to the search.
\end{enumerate}
It converts the gradient function and the learning rate into a step
function, calls the Descent algorithm and returns the final candidate
as well as the remaining unallocated steps.

It should be noted that this definition of Gradient Descent does not
cover Stochastic Gradient Descent.  That is because it does not allow
the algorithm to sometimes ascend.  On the other hand Stochastic
Gradient Descent may not always descend while still guarantying
gradient descent to the limit.  More on the matter is discussed in
Section~\ref{sec:related_work}.

\subsection{Linear Regression}
The Linear Regression algorithm takes the following inputs:
\begin{enumerate}
\item a data set to explain, a matrix of inputs and a column vector
  of outputs;
\item a learning rate, also called step size;
\item an initial candidate to start the search from;
\item a maximum number of steps allocated to the search.
\end{enumerate}
It defines a sum-of-squared-errors-based loss and gradient functions
for that data set, calls Gradient Descent and returns the final
candidate as well as the remaining unallocated steps.

\subsection{Logistic Regression}
The Logistic Regression algorithm takes in input:
\begin{enumerate}
\item a data set to explain, a matrix of inputs and a Boolean column
  vector of outputs;
\item a learning rate, also called step size;
\item an initial candidate to start the search from;
\item a maximum number of steps allocated to the search.
\end{enumerate}
It defines a cross-entropy-based loss and gradient functions for that
data set, calls Gradient Descent and returns the final candidate as
well as the remaining unallocated steps.

\subsection{Logistic-Linear Regression}
The Logistic-Linear Regression algorithm takes the following inputs:
\begin{enumerate}
\item a data set to explain, a Boolean matrix of inputs and a Boolean
  column vector of outputs;
\item a learning rate, also called step size;
\item an initial candidate to start the search from;
\item a maximum number of steps allocated to the search.
\end{enumerate}
It transforms the data set so that the column vector of outputs
represents the odds of outputting True instead of a Boolean value,
calls linear regression on that transformed data set and returns the
final candidate as well as the remaining unallocated steps.

\section{Verification of AI Algorithms}

The concept of verifying properties of AI algorithms is very broad.
It could be verifying AI algorithms themselves, or abstract properties
thereof, their output models, using either crisp mathematical
properties or empirically based ones, or combinations thereof.  In
this work we have focused exclusively on crisp mathematical properties
on AI algorithms.

\subsection{Descending Property for Descent}
The simplest property we could imagine in this situation is that the
algorithm must descend, or at least not ascend.  In other words, that
the final candidate must be better, or at least not worse, that the
initial one.  This may seem like an overly simplistic property, and it
is.  However, as we will see, working with that was already quite an
educational journey.

Let us begin by showing the Idris implementation of Descent, or rather
a slightly simplified version modified for expository purpose:
\begin{minted}[mathescape]{idris}
descent : Ord cost_t =>
          (cnd_t -> cost_t) ->    -- Cost function
          (cnd_t -> cnd_t) ->     -- Step function
          (cnd_t, Nat) ->         -- Init candidate, steps
          (cnd_t, Nat)            -- Final candidate, steps
descent _ _ (cnd, Z) = (cnd, Z)
descent cost next (cnd, S k) = if cost (next cnd) < cost cnd
                               then descent cost next (next cnd, k)
                               else (cnd, (S k))
\end{minted}
It essentially expresses that, given enough steps left, if the cost of
the next candidate is less than the cost of the initial candidate, it
should recursively descend from the next candidate, otherwise return
the initial candidate.  Note that \texttt{cnd\_t} and \texttt{cost\_t}
are type variables, that is they may be substituted by any type, up to
some constraints, at function call.  The descending property can then
be formalized as follows:
\begin{minted}[mathescape]{idris}
descent_le : Ord cost_t =>
             (cost : cnd_t -> cost_t) -> -- Cost function
             (next : cnd_t -> cnd_t) ->  -- Step function
             (cas : (cnd_t, Nat)) ->     -- Init candidate, steps
  (cost (fst (descent cost next cas)) <= cost (fst cas)) === True
\end{minted}
which expresses that the cost of the final candidate should be less
than or equal to the cost of the initial candidate\footnote{For
  information, \texttt{===} denotes the equality type, a dependent
  type with \texttt{Refl} as sole constructor corresponding to the
  reflexivity axiom of equality.}.  Obviously such property should be
trivial to prove given how the algorithm has been written.  In
practice however, it is not so much so, for two reasons:
\begin{enumerate}
\item Idris makes no assumption about the comparison operators
  \texttt{<}, \texttt{>}, \texttt{<=} and \texttt{>=}.  The interface
  \texttt{Ord} guaranties that \texttt{cost\_t} implements these
  operators, but not how they should behave.  Thus one needs to encode
  these assumptions and make sure that they are true for the types of
  interest, which is not always easy, or even possible, especially for
  primitive types like \texttt{Double}.
\item Since the algorithm is recursive, it requires a recursive proof.
\end{enumerate}
To address the first point we added a number of functions formalizing
the standard axioms of total strict and non-strict orders of
\texttt{<}, \texttt{>}, \texttt{<=} and \texttt{>=}.  A small snippet
is given below:
\begin{minted}[mathescape]{idris}
||| Assume that < is irreflexive
lt_irreflexive : Ord a => {0 x : a} -> (x < x) === False
lt_irreflexive = believe_me ()

||| Assume that < is connected
lt_connected : Ord a => {0 x, y : a}
                     -> (x < y) === False
                     -> (y < x) === False
                     -> x === y
lt_connected _ _ = believe_me ()

||| Assume that <= is reflexive
le_reflexive : Ord a => {0 x : a} -> (x <= x) === True
le_reflexive = believe_me ()

||| Assume that <= is transitive
public export
le_transitive : Ord a => {0 x, y, z : a}
                      -> (x <= y) === True
                      -> (y <= z) === True
                      -> (x <= z) === True
le_transitive _ _ = believe_me ()
\end{minted}
The \texttt{believe\_me} function is provided by Idris especially for
these situations.  Also, it should be noted that equality properties
like \texttt{(x <= y) === True} can be sugared into inequalities, but
we decided to stay as close as possible to the Idris core language for
starter.  The whole list of axioms can be found in
file~\href{https://github.com/singnet/ai-dsl/blob/master/experimental/ai-algorithms/descent/Search/OrdProofs.idr}{OrdProofs.idr}
of the~\href{https://github.com/singnet/ai-dsl}{ai-dsl} repository.
We also attempted to use an existing library from Stefan H\"ock
called~\href{https://github.com/stefan-hoeck/idris2-prim}{idris2-prim},
but decided to write our own to maintain as much control as possible.\\

The proof of \texttt{descent\_le}, slightly simplified to suit our
simplified version of \texttt{descent}, is presented below.  Let us
first deal with the base case where the number of allocated steps is
zero:
\begin{minted}[mathescape]{idris}
descent_le _ _ (_, Z) = le_reflexive
\end{minted}
In order to prove the descending property it suffices to invoke the
reflexivity of \texttt{<=} since for that case \texttt{descent} merely
becomes the identity function.  Let us now examine the recursive case
where the number of allocated steps is greater than zero:
\begin{minted}[mathescape]{idris}
descent_le cost next (cnd, S k)
           with ((cost (next cnd)) < (cost cnd)) proof eq
  _ | True = let des_le_nxtcst = descent_le cost next (next cnd, k)
                 nxtcst_le_cst = le_reflexive_closure_lt (Left eq)
              in le_transitive des_le_nxtcst nxtcst_le_cst
  _ | False = le_reflexive
\end{minted}
The proof considers the two branches of the conditional.  If the
condition is false then invoking the reflexivity of \texttt{<=}
suffices for the same reason as above.  If the condition is true then
the proof needs to combine axioms about comparison with the recursion
of \texttt{descent\_le} and the transitivity of \texttt{<=}.

That simplified proof is already somewhat substantial, likely too
substantial to be rapidly discovered by a greedy proof search
algorithm.  The non simplified version of Descent, as well as the
proof of its descending property, is about twice the size of the
simplified one, and can be found in
file~\href{https://github.com/singnet/ai-dsl/blob/master/experimental/ai-algorithms/descent/Search/Descent.idr}{Descent.idr}
of the~\href{https://github.com/singnet/ai-dsl}{ai-dsl} repository.
Discovering such a proof automatically, or semi-automatically, would
still remains relatively practical, either by requiring human
intervention, using proof tactics or more sophisticated inference
control techniques~\cite{Goertzel2014EGI2Chapt18}.

\subsection{Descending Property for Other Algorithms}
Once the descending property has been proved for Descent, proving it
for the remaining algorithms is now truly trivial, for the most part
anyway.

Let us provide an example for Gradient Descent, starting by recalling
what is the gradient descent algorithm.  Given a loss function $L$ and
a learning rate $\eta$, the gradient descent algorithm works by
updating the candidate $\beta$ as follows
$$\beta := \beta - \eta \nabla L(\beta)$$
in other words, the step function takes the opposite direction of the
gradient by a factor of $\eta$.  The Idris code of Gradient Descent is
given below:
\begin{minted}[mathescape]{idris}
gradientDescent : (Ord a, Neg a) =>
  (cost : ColVect m a -> a) ->          -- Cost function
  (grd : ColVect m a -> ColVect m a) -> -- Gradient
  (eta : a) ->                          -- Learning rate
  (cas : (ColVect m a, Nat)) ->         -- Init candidate, steps
  (ColVect m a, Nat)                    -- Final candidate, steps
gradientDescent cost grd eta = descent cost (fsgrd grd eta)
\end{minted}
where \texttt{fsgrd} is a function that takes a gradient,
\texttt{grd}, a learning rate, \texttt{eta}, and produces the step
function described above.  The type of a candidate for Gradient
Descent is now more specific.  Instead of being the variable type
\texttt{cnd\_t}, it is a column vector of size \texttt{m} and type
\texttt{a} represented by \texttt{ColVect m a}.

The descending property for Gradient Descent is expressed as follows:
\begin{minted}[mathescape]{idris}
gradientDescent_le : (Ord a, Neg a) =>
  (cost : ColVect m a -> a) ->           -- Cost function
  (grd : ColVect m a -> ColVect m a) ->  -- Gradient
  (eta : a) ->                           -- Step size
  (cas : (ColVect m a, Nat)) ->          -- Init candidate, steps
  (cost (fst (gradientDescent cost grd eta cas)) <= cost (fst cas))
   === True
\end{minted}
And its proof is simply
\begin{minted}[mathescape]{idris}
gradientDescent_le cost grd eta = descent_le cost (fsgrd grd eta)
\end{minted}
that is the proof of the descending property of Descent. Idris is able
to directly reuse it because it automatically applies the rule of
replacement in the type definition on the function calls present in it
by using their definitions.  So for instance
\begin{minted}[mathescape]{idris}
(cost (fst (gradientDescent cost grd eta cas)) <= cost (fst cas))
\end{minted}
is automatically replaced by
\begin{minted}[mathescape]{idris}
(cost (fst (descent cost (fsgrd grd eta) cas)) <= cost (fst cas))
\end{minted}
which is what \texttt{descent\_le} proves.

Proving the descending properties on the other algorithms, with the
exception of Logistic-Linear Regression, is equally trivial.  Proving
it for Logistic-Linear Regression requires an explicit use of the rule
of replacement.

\chapter{Program Synthesis}
\label{chap:program_synthesis}

Program synthesis is at the core of a number of functionalities of the
AI-DSL, such as AI services composition and fuzzy matching.  During
that phase we have explored a number of ways to achieve program
synthesis that we are going to detail now.

\section{Language Framework}

We started by experimenting with building our own language framework
in order to represent any language, including its type system, given a
description of its syntax and its operational semantics.  The
advantage of such approach is that program synthesis algorithms can be
developed in a manner that is somewhat language agnostic.
Additionally, since that language framework is implemented in Idris
and programs are represented as data, Idris can actually be used for
program synthesis by relying on a built-in functionality call Proof
Search.

The code for that experiment can be found in
folder~\href{https://github.com/singnet/ai-dsl/blob/master/experimental/program-synthesis/language-framework}{language-framework}
of the~\href{https://github.com/singnet/ai-dsl}{ai-dsl} repository.
We did not have enough time to really experiment with language
agnostic program synthesis as we initially planned, however we were
able to leverage Idris built-in program synthesis as explained in
Section~\ref{subsec:AST}.

\section{Idris Elaboration}

Idris supports reflective programming via
the~\href{https://www.idris-lang.org/docs/idris2/current/base_docs/docs/Language.Reflection.html}{Language.Reflection}
module.  That is, one can represent Idris programs as data and thus
implement program synthesis of Idris programs in Idris.  Idris Proof
Search, further described in Section~\ref{sec:idris-proof-search},
relies on that.  However, due to a number of current limitations of
Idris Proof Search, we estimated that we should take a deep dive into
that module, as well as a complementary library by Stefan H\"ock
called~\href{https://github.com/stefan-hoeck/idris2-elab-util}{idris2-elab-util}.

Only partial success was achieved with that method by synthesizing
nullary programs given its output type.  However, it already showed
promises and we may want to revisit this experiment later on.  The
code can be found in
folder~\href{https://github.com/singnet/ai-dsl/blob/master/experimental/program-synthesis/idris-synthesis}{idris-synthesis}
of the~\href{https://github.com/singnet/ai-dsl}{ai-dsl} repository.

\section{Idris Proof Search}
\label{sec:idris-proof-search}

Since recently, Idris2 has introduced a functionality called Proof
Search.  Contrary to what its name suggests it can be used for program
synthesis, not just proof search -- which should be no surprise to
those familiar with the Curry-Howard correspondence.  It has however,
at the time of writing this document, a number of downsides.  The main
one being it can only have access to
\begin{enumerate}
\item data type constructors,
\item variables in its current environments.
\end{enumerate}
Meaning, it does not have access to functions or constants defined in
the current and imported modules.  The other downsides are that it is
poorly documented and difficult to control, likely due to having being
introduced recently.

Nonetheless, in this section we explore how such functionality can be
used for program synthesis in spite of its current limitations.

\subsection{Program Synthesis with Abstract Syntax Trees}
\label{subsec:AST}

The idea is to represent programs as Abstract Syntax Trees.  Each
operator can be represented as a constructor of that data structure of
that Abstract Syntax Tree, which Idris can access to generate trees
representing programs.  Here is a minimal example:
\begin{minted}[mathescape]{idris}
||| Abstract Syntax Tree Types
data Ty = TyDouble | TyCandidate | TyFun Ty Ty

||| Abstract Syntax Tree Terms
data Expr : Ty -> Type where
    Candidate : Expr TyCandidate
    Loss : Expr (TyFun TyCandidate TyDouble)
    Gradient : Expr (TyFun TyCandidate TyCandidate)
    Descent : Expr (TyFun TyCandidate TyDouble) ->
              Expr (TyFun TyCandidate TyCandidate) ->
              Expr TyCandidate ->
              Expr TyCandidate
\end{minted}
External functions found in libraries, or in our case remote AI
services, would be represented as constructors of \texttt{Expr}, such
as \texttt{Loss}, \texttt{Gradient} and \texttt{Descent}.  Then one
can ask Idris to fill the hole of a definition, such as
\begin{minted}[mathescape]{idris}
linearRegression : Expr TyCandidate
linearRegression = ?hole
\end{minted}
which it successfully does by suggesting a number of candidates to
replace \texttt{?hole} by, such as
\begin{minted}[mathescape]{idris}
Candidate
Descent Loss Gradient Candidate
Descent Loss Gradient (Descent Loss Gradient Candidate)
...
\end{minted}
The second suggestion corresponds to implementation of linear
regression we are looking for.

\subsection{Program Synthesis with Variables}

Let us now explore using environment variables to represent constants
and functions instead of constructors.  The meta-function \texttt{syn}
described below:
\begin{minted}[mathescape]{idris}
syn : (a -> b -> c) ->
      (a -> b -> c) ->
      (a -> b -> c) ->
      a -> b -> c
syn f g h x y = ?hole
\end{minted}
and takes 3 functions, \texttt{f}, \texttt{g} and \texttt{h}, as
arguments, and outputs a function that takes 2 arguments of types
\texttt{a} and \texttt{b} respectively.  Idris successfully fills the
hole by suggesting the following candidates
\begin{minted}[mathescape]{idris}
h x y
g x y
f x y
\end{minted}
covering all possibilities in that instance.

Here is another example attempting to reproduce the one using Abstract
Syntax Trees provided in Section~\ref{subsec:AST}.
\begin{minted}[mathescape]{idris}
syn : (cnd -> cnd) ->                          -- Step function
      ((cnd -> cost) -> (cnd -> cnd) -> cnd -> cnd) -> -- Descent
      (cnd -> cost) ->                         -- Cost function
      cnd ->                                   -- Init candidate
      cnd                                      -- Final candidate
syn n d c i = ?hole
\end{minted}
Idris again finds the candidate we are looking for, that is the second
suggestion in the list below:
\begin{minted}[mathescape]{idris}
i
d c n i
d c n (d c n i)
...
\end{minted}
where \texttt{d}, \texttt{c} and \texttt{n} are variables referencing
to the descent, cost and step functions respectively, and \texttt{i}
is the initial candidate.

The full experiments can be found in
folder~\href{https://github.com/singnet/ai-dsl/blob/master/experimental/program-synthesis/idris-proofsearch}{idris-proofsearch}
of the~\href{https://github.com/singnet/ai-dsl}{ai-dsl} repository,
and contain more attempts including unsuccessful ones using the
\texttt{let} keyword not covered here.  Of course these experiments
are both simplistic and too unconstrained to narrow down the search to
the correct candidate, but the fact that they work at all indicates
that synthesizing programs, with more operators and types, including
dependent types representing properties, should be possible with
standalone Idris.  And as Idris Proof Search functionality improves,
it might even become a viable option in practice.  Other options that
would be worth exploring would be to experiment with the Proof Search
functionalities of other DTLs such as AGDA and Coq, or, as mentioned
in the \ref{sec:related_work} Section, program synthesis with Liquid
Haskell.

\section{Coevolutionary Intelligent Agent System}

Another approach, derived from SISTER~\cite{Duong2004} and being
currently developed in SingularityNET, not initially based on
dependent types but heavily focused on collective emergent behaviors,
including emergent communication and typing, is described below.

In the usecase for longevity, Singularity Net spinoff
\href{https://rejuve.ai/}{Rejuve.AI} will use AI-DSL in tandem with a
coevolutionary multi intelligent agent reinforcement learning
algorithm, the Generative Cooperative Network (GCN), to combine
crowdsourced models into a dynamic multiresolutional mechanistic model
of the human body.  Here it will do model synthesis rather than
program synthesis, putting together generative Bayesian, neural and
simulation models and data from separate studies into a coherent
whole.  The GCN will do implicit typing, that automatically
categorizes models into groups of similar implicit requirements for
sucess, where the measure of success is the amount of simulated tokens
a model can win from multiple simulated challenges in a simulated
market. Agents compete to win challenges but also cooperate in that
they employ each others services, to delegate specialized knowledge to
other "expert" models. Agents learn a system of signs that come to
represent their emergent role category and the requirements that go
along with those roles.  The system of roles is the agent "culture", a
functional semantic space that scaffolds other agents, including new
agents that have not converged yet, along a path that leads them to
the solutions that other agents have found in the past. However
scaffolded, and however reachable by evolutionary computation,
traveling along such a path is done by trial and error. Agents have
classified themselves into types, the signs of which exist in a
functional semantic space. However, the sign is limited in that it
must basically be memorized. It is only rewarded when it is learned
correctly, relative to other agents.

This sort of approach can carry us a significant distance toward
modeling longevity related data, but it is likely to reach its
limits. In order for the agent culture to contain open ended
intelligence, it can not learn everything by trial and error: rather,
the emergent type ontology will need to somehow be made explicit and
carry with it explicit instructions on requirements. This becoming
explicit is one of the ways in which signs in the GCN encourage open
ended emergence. For this we can leverage the AI-DSL strategy for
agent typing.  Hyperon’s pattern miner, as well as more general forms
of reasoning such as that offered by PLN~\cite{Goertzel09PLN}, will
assist in finding what it is about the agents displaying a role sign
which enables its teams to make a profit.  PLN inference will express
this in AI-DSL, which Hyperon will use to compose the answer from user
contributed models, and formally verify exactly what those models do.
The implicit (emergent sign) and explicit AI-DSL methods that GCN
agents use are complementary and help each other. The implicit sign
method focuses selective pressure on agents long enough for choices to
be objectified into institutions so that they are consistent and
widespread enough for explication. Implicit signs supply the explicit
algorithms with enough examples of emergent capabilities in the
ecosystem to infer upon. Explication takes away some of the burden of
memorization of implicit signs by trial and error for new agents, so
signs can indicate emerging requirements while explicit rules indicate
requirements that have already become objectified institutions. Agents
and the signs that they display will be fed to the explicit algorithm
which will use Hyperon's pattern mining to interpret the implicit
sign's explicit meaning, through an examination of the behaviors of
the agents that display the sign. Once explicit, the hyperon
formalization of the sign is a directive that is implementable by
agents new to an agent ecosystem, that no longer need to learn the
meaning of those particular signs by trial and error.

\chapter{Conclusion}

\section{Related Work}
\label{sec:related_work}

Here's a list of projects and publications we have discovered along
the way that relate to the work done during that iteration.

\subsection{Machine Learning Formal Verification}

Over the recent years, and to the best of our knowledge, only a small
number of publications have appeared on the application of formal
verification to either machine learning algorithms or machine learned
models.  The most relevant work we have found so far is described in a
paper entitled \emph{Developing Bug-Free Machine Learning Systems With
  Formal Mathematics}~\cite{DBLP:journals/corr/SelsamLD17}.  In that
paper a formal specification of a class of stochastic gradient descent
algorithms operating on stochastic computation graphs is implemented
in Lean~\cite{Lean}, alongside a property expressing that the back
propagation correction points, in average, towards the gradient
descent of the cost.  Mathematically, this may be expressed by the
following equality
$$\mathbb{E}_{g,\theta}[\texttt{bprop}(g,\theta,\bold{X})] = \nabla_{\theta}(\mathbb{E}_{g,\theta}[\texttt{cost}(g,\bold{X})])$$
where $g$ is a stochastic computation graph parameterized by $\theta$,
$\bold{X}$ is a random vector describing the values sampled from $g$,
$\texttt{bprop}$ the is back propagation function and $\texttt{cost}$
is the cost function.  Such equality is formally expressed in Lean
using its existing mathematical vocabulary as well newly introduced
one to express notions of probability and measure theory such as
expectation, integration and derivation, then proved using tactics
developed for that purpose.  The authors admit that their prove
assumes infinite-precision real numbers as opposed to finite-precision
floating point numbers used in practice.  However, they point to a
couple of papers addressing the use of floating point numbers in the
context of automatic theorem proving~\cite{Harrison2006,
  Ramananandro2016}.

Another related work presented in~\cite{Bagnall2019} aims to prove
properties about learned models, as opposed to learning algorithms.
Formalizing Hoeffding's inequality~\cite{Hoeffding1963} in
Coq~\cite{Bertot2004}, the authors show how to automatically prove the
extend to which a given model, such as a perception, generalizes on
unknown data.

\subsection{Smart Contract Formal Verification}

The subject of formal verification of smart contracts has gathered a
lot more attention.  This may not be so relevant to the AI aspect of
the AI-DSL, but certainly is relevant to the smart contract
interaction aspect that, even though has been somewhat neglected in
our research until now, will likely play an important role eventually.

We first have come across a formal specification of the Ethereum
Virtual Machine (EVM) provided in~\cite{Hildenbrandt2018} using the
$\mathbb{K}$ framework~\cite{Xiaohong2019}, enabling formal
verification based on Reachability Logic~\cite{Alechina2000}.  That
work focuses on a fairly low level to verify whether the EVM operates
according to its specification, as opposed to verifying smart
contracts themselves.

Approaches for doing formal verification on smart contracts, using
higher level languages targeting the EVM, also exist.  In 2016 a
Master's thesis~\cite{Pettersson2016} was conducted to explore how
Idris can be used to write smart contracts avoiding common failures
such as stack overflow or lack of cryptographic encryption when
required.  On top of using Idris to detect such failures, the authors
extended the Idris compiler to support Serpent~\cite{Delmolino2015}, a
high level language for the EVM.  To our knowledge unfortunately that
work has not been pursued any further.  Similarly, a system called,
ConCert~\cite{Annenkov2020} has been developed to do formal
verification of smart contracts written in $\lambda_{smart}$, a
fragment of the \textsc{Acorn} smart contract language, using
Coq~\cite{Bertot2004}.

Another important aspect is the verification of smart contract
compilers.  For instance in~\cite{Krijnen2022} the authors describe an
approach based on \emph{Translation Certification} for Plutus smart
contracts by providing certificates guarantying that the various
stages of transformations from Plutus Intermediate Representation
(PIR) to Plutus Core (PLC), such as dead-code elimination, inlining
and more, do not invalidate high level properties.  Although this
approach is not as thorough as complete compilation certification, it
has the advantage of being more adaptable to compiler evolution.  The
part providing the \emph{Translation Certificates} is implemented in
Coq.

Then they are blockchains that have been created to support formal
verification from the beginning.  Tezos~\cite{Tezos2014}, using
Michelson, a low level stack-based smart contract language, comes with
a formal verification tool called Mi-Cho-Coq~\cite{Bernardo2019}
developed in Coq.  Higher level languages targeting Michelson also
exist such as Albert~\cite{Bernardo2020}, an Intermediate Level
Language, and Juvix~\cite{Goes2020} a Dependently Typed Language (DTL)
based on Quantitative Type Theory (QTT)~\cite{Atkey2018} that not only
allows to reason about smart contracts at a high level, but also
produces optimized Michelson code by taking advantage of the
quantitative aspect of QTT.  Likewise,
\textsc{Zilliqa}~\cite{Zilliqa2017} comes with
\textsc{Scilla}~\cite{Ilya2018}, an intermediate-level language
enabling formal verification with Coq.  The Zen
protocol~\cite{Zen2017} is another such example and supports formal
verification via F*~\cite{Swamy2013}.  Notably, the type of
verification described in its white paper includes computational
resources, to formally guaranty that a contract will be allocated
enough gaz before running.  Another interesting blockchain
specifically designed to support formal verification is
RChain~\cite{RChain2021}, further elaboration is provided in Section
\ref{subsec:languages_aidsl}.

In addition, a few more publications can be found in that
study~\cite{Pace2020}, as well as other articles from that same book
of proceedings. In conclusion, it appears to be a rapidly growing
field and there is no doubt that formal verification will
progressively become an indissociable part of the blockchain
technology given the extremely strong financial incentive to create
reliable systems in that context.

\subsection{Program and Proof Synthesis}

One of the most relevant work on program and proof synthesis for
dependent types still seems to be the Idris hand book~\cite{Brady2017}
as well as the more recent paper describing QTT, the new theoretical
foundation of Idris2~\cite{Brady2021}.  The AGDA
tutorial~\cite{Norell2009} is also frequently cited but we have yet to
go through it.

Beside that, we have found a collection of relevant works aim to
address the problem of \emph{Component-Based
  Synthesis}~\cite{Feng2017}, also called \emph{Modular
  Synthesis}~\cite{Heineman2016}.  Meaning, how to synthesize
functions by composing available functions from a large library, such
as typically provided by programming language ecosystems, like C++
STL, Python Standard Library and so on.  In~\cite{Guo2022}, a system
capable of composing RESTful APIs functions to fulfill a given
specification is described.  Since RESTful types are limited, the
system described by the authors begins by enhancing type signatures
with \emph{Semantic Types}, exploiting the RESTful type descriptions
to heuristically replace non-semantic types like \texttt{String} by
semantic types like \texttt{User} or \texttt{Id}.  Then performs
component-based synthesis using \emph{Type Transition Nets}
(TTN)~\cite{Feng2017}, a special kind of Petri Nets.  Since Semantic
Types are still rather limited, at least compared to Dependent Types,
they also use input-output examples to further narrow down the search.
TTN-based synthesis works well on \emph{Concrete Data Types}, like
\texttt{List Int}, but not so well on \emph{Abstract Data Types}, like
\texttt{List a} where \texttt{a} is a variable.  To address that a
variation of TTN is introduced in~\cite{Guo2020} called \emph{Abstract
  Transition Network} (ATN).  Such structure is used by
\textsc{Hoogle+}~\cite{Michael2020}, a search engine similar to
\textsc{Hoogle}~\cite{Mitchell2004}, that is, it searches the entire
Haskell Standard Library, but returns small function compositions
satisfying a type signature, instead of standalone functions.
Overall, even though that work is still limited to Non-Dependent Type,
it is nonetheless quite relevant and contains parts that could
potentially be reused for Dependent Types, such as ATN-based
synthesis.

Work towards addressing component-based synthesis using more
expressive types, approaching full blown dependent types, also exists.
The most relevant work seems to be
\textsc{Synquid}~\cite{Polikarpova2016}, a system that can perform
component-based synthesis on functions formally specified with
\emph{Refinement Types}~\cite{Flanagan2006}.  Refinement types are
like regular types decorated with predicates.  Below is an example of
Refinement Type expressing the type of strictly positive integers
$$\{\nu : \texttt{Int}\ |\ 0 < \nu\}$$
They are generally less powerful than dependent types, although it may
depend on the particular systems being compared.  Unlike dependent
types they do not require proof terms, meaning the function
definitions are identical with or without refinement types, only the
types, complemented with predicates when desired, differ.  The
advantage of such approach is that it makes adding refinement types to
existing programs easier.  The inconvenient is that the proofs are
obfuscated, synthesized at compile time by a separate component like
an SMT prover.  In comparison dependent types treat proofs and
programs on the exact same footing.  It means that any synthesis
method developed for programs de facto works on proofs and vice versa.
Beside giving full visibility to the proofs, this also gives more
freedom of action when synthesis requires assistance.  That is said,
refinement types can be very expressive and component-based synthesis
already exists for that class thus they should be given carefully
consideration.

Another aspect relates to formalizing computational costs and such,
which can influence program synthesis by discarding candidates that do
not operate within those constraints.  The system
\textsc{Resyn}~\cite{Knoth2019} is an example of that where a more
efficient algorithm to calculate the common elements between sets is
discovered by incorporating computational costs is the formal
description.

It is also worthwhile mentioning some work aiming at providing a
type-theoretic interpretation of example-directed~\cite{Frankle2016}.
This provides some foundation for how formal specifications can be
composed of abstract mathematical properties mixed with concrete
examples.  There is no doubt such mixture will be very useful for the
AI-DSL.  Of course in addition we will need to go further by
introducing statistical properties as opposed to crisp mathematical
properties, as theoretically explored in~\cite{Warrell2016} for
Dependent Types.

Program Synthesis can also be guided by large language models, as in
Jigsaw~\cite{Jain2022}, which uses a \emph{Pre-Trained Large Language
  Model} (PTLM) such as GPT-3~\cite{Brown2020} or
Codex~\cite{Chen2021} to synthesize functions based on an inform
specification provided in natural language, such as \texttt{``Delete
  every third row of the given table''}.  Since PTLMs have not been
built to operate on programming languages, it requires some amount of
pre and post processing to make it work.  The pre-processing consists
in selecting a context to inform the PTLM of the task at hand to
solve.  The context is a pairs of questions and answers, $(Q_i, A_i)$,
such that $Q_i$ is an informal specification and $A_i$ is a program.
Then a new informal specification $Q$ is provided to the PTLM which
should output the corresponding program $A$.  Most of the time the
output program is neither syntactically nor semantically correct.
Thus a series of post-processing transformations needs to take place
to repair it.  Syntactic corrections can be guided by the programming
language grammar while semantic corrections can be guided by a set of
examples $A(x_j)=y_j$, as well as the signatures of the functions
involved in the synthesis to correct the types and the number of
arguments.  This technique has been applied to the Pandas Python
library, thus on a non-dependently type system, with some descent
level of success.

Another project involving learning for guiding program synthesis is
\textsc{Probe}~\cite{Barke2020}, an Inductive Program Synthesizer,
thus based solely on examples, using efficient bottom-up synthesis by
pruning the search space using
\begin{enumerate}
\item \emph{Observational Equivalence}.  Observational equivalence is
  a partial form of semantic equivalence based solely on examples.
\item \emph{Size-Based} instead of \emph{Depth-Based} enumeration.
  They justify that with the observation that ``\emph{useful programs
    tend to be skinny rather than bushy}''~\cite{}.
\item Production guided by a Probabilistic Context-Free Grammar (PCFG)
  built based on partial solutions.
\end{enumerate}
The latter is where learning takes place.  The rational is that
programs that are correct on a subset of examples, that is compute the
correct outputs for a subset of inputs, are likely to be used, wholly
or partly, by programs that are correct on the complete set of
examples.  As soon as such partially correct programs are discovered,
the PCFG is updated to give these programs, as well programs using
similar production rules, higher probabilities.  They successful
outperformed a number of existing systems on a limited
representational language.  Probably the main drawback is the use of a
context-free, as opposed to context-sensitive, grammar to represent
the distribution of good programs.  The advantage being that
overfitting is less likely to be introduced in such model.  Their
system is implemented in Scala.  One may also cite~\cite{Ozkural2011}
as another attempt to use a PCFG, this time to learn the distribution
of good programs from a sequence of problems and subsequently guide
program synthesis for future problems.  Attempts to use more powerful
models also exist such as MOSES~\cite{Looks2006},
WILLIAM~\cite{Franz2022}, as well the yet unpublished work on
Inference Control Meta-Learning~\cite{Geisweiller2017,
  Geisweiller2018} conducted at the SingularityNET Foundation.

As a complement to program synthesis, an increasingly active field of
research pertains to specification synthesis, both formal and
informal.  For formal specification synthesis we may mention this work
using Liquid Types, short for \emph{Logically Qualified Data
  Types}~\cite{Rondon2008}.  Liquid Types are a decidable fragment of
Refinement Types.  Their system is able to automatically infer the
correct specifications of all functions of an Array OCAML library.  In
the course of their work, a bug from that library that had remained
hidden for a long time was revealed and corrected in the process.
This research could potentially be useful to infer the specifications
of existing AI services that can then be manually corrected, which is
easier than having to write a specification from scratch.  For
informal specification synthesis, large language models have been used
as well.  In~\cite{Khan2023} the authors use Codex to infer function
descriptions in English for a variety of popular programming
languages, and manage to get competitive performances with one-shot
learning.

It can be noted that a lot of the work cited above uses Haskell or
extensions thereof.  However, to the best of our knowledge there is,
as of the time of this writing, no method for component-based
synthesis using dependent types.  Which is precisely what we need for
the AI-DSL.

\subsection{Languages for the AI-DSL}
\label{subsec:languages_aidsl}

The AI-DSL will likely be made of at least two languages
\begin{enumerate}
\item a back-end language targeting the power user, doing the heavy
  lifting of program, proof, and possibly specification synthesis and
  checking;
\item a front-end language for the regular user.
\end{enumerate}
So far we have explored using Idris as back-end language, but there
are other choices.  The reader may have noticed above languages such
as Lean, Coq and F*.  We still have to fully examine the pros and cons
of each language.  However already some observations can be made.
Lean and Coq are more oriented towards proving mathematical theorems,
while Idris is more oriented towards writing and verifying programs.

The advantage of Idris, as we have experienced first hand, is that
proofs and programs are based on the same language, and share much
vocabulary.  For instance the function \texttt{map}, from the
\texttt{Functor} interface, may be used inside proofs or programs
alike.  Beside being very elegant, it brings the notion of reusability
to a whole new level.  AGDA~\cite{Norell2009} also shares that
quality, though seems to be more oriented towards mathematics and less
towards programming compared to Idris.  Finally, as we have seen,
Juvix~\cite{Goes2020}, although dedicated to smart contract
programming, is foundationally close to Idris as it is also based on
QTT~\cite{Atkey2018}.  It is a fairly new language and we will want to
keep a close eye on it, because ultimately the AI-DSL will have to
interface with smart contracts and Juvix already does that.

Lean and Coq, due to being more oriented towards mathematics, have
also their advantages, such as having large libraries of mathematical
theories that can be reused when proving properties of programs.
There is no doubt that the Idris mathematical library will grow
consequently over time, but as of today it is lagging behind.

All these languages above are Dependently Typed Languages.  Another
class of expressive languages are based on Refinement Types.  Even
though Dependent Types are generally superior to Refinement Types, as
far as we have seen, tools for synthesizing programs and
specifications using Refinement Types are currently more mature than
tools using Dependent Types.  Thus, although Dependently Typed
Languages may be be better in the long run, languages based on
Refinement Types like Liquid Haskell~\cite{Vazou2014}, may provide
more benefits in the immediate term.  Another, perhaps shallow but
potentially meaningful reason to use Haskell, is that
Plutus~\cite{Plutus2022}, Cardano's smart contract language, is
heavily based on Haskell.  More exploration on the matter is expected
to take place during the next phases to measure the pros and cons of
these various languages.  But it should also be noted that our current
choice, Idris, is planned to be eventually supplanted by
MeTTa~\cite{Warrell2022}, own home brewed language being built for
Hyperon, the next generation of the OpenCog Framework.

Finally, you may have noticed that all these languages are functional,
but there are other classes of languages that could potentially be
used as well.  Process calculi, such as the $\pi$-calculus and the
$\rho$-calculus~\cite{Meredith2005} are some examples.  These calculi
make especially sense in highly distributed environments.  In
particular, it should be noted that the $\rho$-calculus is used as
foundation of Rholang~\cite{Rholang2021}, a smart contract language
for RChain~\cite{RChain2021}, a blockchain technology that is heavily
focused on concurrency and scaling.  Process calculi also have strong
type theory foundations, such as Behavioral and Spatial
Types~\cite{Caires2004}, as well as a novel approach called Native
Types~\cite{Williams2021}, that can auto-generate an expressive type
systems given essentially any calculus.  Finally, since it is clear
that component-based synthesis is compositional by nature, process
calculi also fit well that requirement.  Other languages built on
composition as their primitive operators are also worth exploring.
For instance the Kihi language~\cite{Timothy2018} is half-way between
a \emph{Concatenative Language}, highly compositional by nature, like
Forth and a traditional functional programming language like Haskell.
The advantage of Kihi over Forth is that no stack is required, which
makes it more amenable to formal verification.

So there is a lot to explore.  Fortunately we do not need to come to
the end of what seems to be a never ending exploratory rabbit hole to
start prototyping the AI-DSL, which we intend to do as soon as the
next phase begin.  We do intend however to keep exploring the various
avenues put forth in that section in parallel of that prototyping
work.

\section{Future Work}
This work has just been scratching the surface.  Let us explore the
developments that the foreseeable future may bring.

\subsection{Shortcomings and Solutions}
Regarding formal specification of AI algorithms, what we have done in
this work is very minimal.  We have only formalized a descending
property and a lot more is needed.  For gradient descent, the exact
set of properties we may want to formalize is yet to be determined,
but could include:
\begin{itemize}
\item The gradient function provided to the gradient descent algorithm
  is, or approximates, the actual derivative of the cost function.
\item Cost functions are sum of squared errors in the case of linear
  regression and cross-entropy in the case of logistic regression,
  measure information losses.
\item Cost functions have certain topology, such as convex.  This is
  useful to know for instance if the resulting candidate approximates
  the global optimum or not.
\item The models are linear in the case of linear regression.
\end{itemize}
These are just examples of properties that are immediately applicable
to our AI algorithms.  More broadly there are many more properties of
interest, pertaining not only to the algorithms themselves but as they
interact with the real world.  This brings the need for an ontology as
explained in the previous report~\cite{AIDSLReport2021}.  Other
properties driven by real world use could include for instance
avoiding introducing backdoors during training~\cite{Menisov2022}.
There are many more examples, the breadth and utility of what can be
formalized is simply enormous.

\subsection{Axioms and Uncertainty}
They are a few of problems regarding the assumptions about the
comparison operators \texttt{<}, \texttt{>}, \texttt{<=} and
\texttt{>=} that, in the case of \texttt{Double}, are known to be
incorrect due to imprecision errors and handling of special cases such
as \texttt{inf} and \texttt{nan}.  It's not entirely clear yet how
that should be addressed.  One way could be to replace \texttt{Double}
by an arbitrary precision floating number data type.  The problem is
that such data type can have a high computational overhead, and most
existing AI algorithms do not use that anyway.  Another solution would
be to refine the axioms of \texttt{Double} to account for these errors
and special cases.  A third solution would be to account for
uncertainties, more on that below.

Then, the algorithms presented here are deterministic.  However it is
often the case that nondeterministic algorithms are preferable.  For
instance one may want to use stochastic gradient descent to avoid
local optima.  In that case the descending property should be replaced
by a stochastic descending property, as done
in~\cite{DBLP:journals/corr/SelsamLD17}.  This brings us to the
importance of supporting probabilistic specifications more generally.
This is especially relevant to AI algorithms that are not only often
nondeterministic but also have their performances typically measured
in terms of their fitness to the real world, which is intrinsically
and profoundly uncertain.  Fortunately, to address that, logic
frameworks such as Probabilistic Logic Networks~\cite{Goertzel09PLN}
can be used.

\subsection{More, More and More Algorithms}
In the long run we want to provide formal specifications to \emph{all}
AI algorithms, ranging from the most specialized, such as Cyclical
Stochastic Gradient Markov chain Monte Carlo for Bayesian Deep
Learning~\cite{Zhang2020}, to the most general, such as Solomonoff
Universal Induction~\cite{Solomonoff1964}.  Of course we, the members
of the AI-DSL team, cannot do it all by ourselves.  This is a
monumental task that will have to be progressively outsourced to the
community, and eventually to the network itself.  The latter has the
interesting ramification that the network should progressively take
the role of an AI researcher conceiving its own AI algorithms in a
justified and principled way.  For starter, however, it is important
that we provide an initial kernel that can be used in practical
applications as well as to serve as didactic examples for the
community.

\subsection{Program Synthesis}

For the long term is seems somewhat unavoidable we will need to build
our own program synthesizers.  That would probably give us the
greatest amount of control which is especially important for
addressing the inherent combinatorial explosion associated with
program synthesis.  Fortunately, that is exactly the things that we,
the broader SingularityNET research and development team, are working
on via the development of OpenCog Hyperon and MeTTa.  For the short
term however, we want to rely on existing solutions, such as Idris
Proof Search, which might entail investing some of our efforts to
improve it, or discovering unconventional ways to use it to work
around its limitations.

\subsection{Work Planned for the Next Phase}

The previous phases were mainly about building an understanding of the
various challenges ahead, such as how to use dependent types and
program synthesis to achieve autonomous AI services composition.  In
the next phase we intend to put this understanding into practice to
ideally create a limited yet functional prototype of the AI-DSL.
Below is a tentative, subject to change, description of the steps
involved in creating such prototype.

\begin{enumerate}
\item Build the necessary tools for releasing an Idris-based SDK for
  the AI-DSL.  Such SDK would initially target the power user.  It may
  contain an Idris library exposing existing AI services from the
  SingularityNET market place.  Such library should be automatically
  generated by crawling the market place and turning protobuf
  specifications into Idris type signatures.  An offline AI-DSL
  Registry of some sort.
\item For starter, the AI service formal descriptions may be reduced
  to regular types, as that is what protobuf offers.  This should
  already enable the user of the AI-DSL SDK to easily call and compose
  AI services.  Such AI service compositions should then be
  publishable back to the SingularityNET market place.  By extension,
  any AI algorithms implemented in Idris, like the ones implemented
  during phase 2, should be easily publishable to the market place as
  well.
\item The AI-DSL SDK could be tested on some of the service
  compositions described in
  the~\href{https://github.com/singnet/ai-dsl/blob/master/doc/technical-reports/2022-Oct/snet-service-assemblages.pdf}{snet-service-assemblages.pdf}
  document living within that same folder, such as the one converting
  an English song to a Chinese song as described in Section 2.5 of
  that referenced document, by splitting vocals and instruments,
  translating English singing into Chinese singing and layering the
  result back onto the instruments.
\end{enumerate}
Once all this work has been accomplished, if time permits,
improvements could be made on the following fronts.
\begin{enumerate}
\item Refine the protobuf-based specifications with Dependent Types.
  This may as well entail using an ontology, like SUMO, to replace
  general types like Bytes by more semantic types like Audio.
\item Integrate computational and financial cost in the formal
  specification, as well as performance evaluations and their
  compositional laws.
\item Improve Idris program synthesis to be geared towards
  composition-based synthesis involving a large number of functions.
\item Create a dedictated front-end language, the AI-DSL per se, as
  opposed to using Idris.  Such language could be especially suited to
  represent composition, specifications, and designed to accommodate
  the regular user, not just the power user.
\item Make progress towards replacing the Idris back-end by, or
  complementing with, Hyperon/MeTTa.
\end{enumerate}

\section{Acknowledgments}

Thanks to Alexey Potapov, Eyob Yirdaw, Hedra Yusuf, Michael Duncun,
Jonathan Warrell, Douglas Miles, Abdulrahman Sermie, Robert Haas and
Ben Goertzel for their feedback, suggestions and discussions during
that phase.  Thanks to the SingularityNET Foundation and Cardano
Project Catalyst for funding that work.

% \appendix
% \chapter{Glossary}
% \begin{itemize}
% \item \textbf{AI service assemblage}: collection of AI services
%   interacting together to fulfill a given function.  Example of such
%   AI service assemblage would be the Nunet Fake News Warning system.
% \item \textbf{Dependent Types}: types depending on values.  Instead of
%   being limited to constants such as \texttt{Integer} or
%   \texttt{String}, dependent types are essentially functions that take
%   values and return types.  A dependent type is usually expressed as a
%   term containing free variables.  An example of dependent type is
%   \texttt{Vect n a}, representing the class of vectors containing
%   \texttt{n} elements of type \texttt{a}.
% \item \textbf{Dependently Typed Language}: functional programming
%   language using dependent types.  Examples of such languages are
%   Idris, AGDA and Coq.
% \item \textbf{DTL}: Shorthand for Dependently Typed Language.
% \end{itemize}

\bibliographystyle{splncs04}
\bibliography{local}

\end{document}
